using System;
using System.Threading;
using System.IO;
using System.Collections.Generic;
using System.Collections;


public class StateHist{
	Object state;
	StateHist parent;
	public StateHist (Object state, StateHist parent)
	{
		this.state = state;
		this.parent = parent;
	}
	
	public Object State {
		get {
			return this.state;
		}
	}
	public StateHist chain(Object newState){
		return new StateHist(newState,this);
	}
	public String fullHistory(){
		return Node.nodeString(state) + "  " + (parent==null ? " << " : parent.fullHistory());
	}
}

public class EqFalseRewrite : Rewrite{
    public EqFalseRewrite() : base(null,"F"){
		
    }	
	public override Dictionary<string, object> unify (object queObj)
	{
		if( queObj is Node ){
			Node nd = (Node)queObj;
			if( nd.Name.Equals("=") && nd.Children.Count==2 ){
				if( !(nd.Children[0] is Node) && !(nd.Children[1] is Node) &&
					!Rewrite.isVar(nd.Children[0]) && !Rewrite.isVar(nd.Children[1]) ){
					if( !nd.Children[0].Equals(nd.Children[1]) ){
						return new Dictionary<string,Object>();
					}
				}
			}
			return null;
		}
		return null;
  }	
}

public class RewritesBase{
	List<Rewrite> rewrites = new List<Rewrite>();
	public RewritesBase(){
		rewrites.Add(new EqFalseRewrite());
	}
	public void add(Node ruleNode){
		Console.WriteLine("importing rule "+Node.nodeString(ruleNode));
		if( ruleNode.Children.Count!=3 ){
			Console.WriteLine("not rule "+Node.nodeString(ruleNode));
		}
		//Node cond = ruleNode.childNode(0);
		Object left = ruleNode.Children[0];
		Object right= ruleNode.Children[1];
		rewrites.Add(new Rewrite(left, right));
		if( Rewrite.findFreeVars(left).IsSubsetOf(Rewrite.findFreeVars(right)) ){
			rewrites.Add(new Rewrite(right, left));
		}
	}
	public void add(/*Node cond,*/ Node q, Object result){
		//Console.WriteLine("adding rewrite to RewriteBase rewrites_old="+rewrites.Count);
		Node rule = new Node("=");
		//rule.add(cond);
		rule.add(q);
		rule.add(result);
		add (rule);
		if( "T".Equals(result) && q.Name.Equals("=") ){
			//  True equality is a ready rewrite
			Node ruleEq = new Node("=");
			//ruleEq.add(cond);
			ruleEq.add(q.Children[0]);
			ruleEq.add(q.Children[1]);
			add (ruleEq);
		}
	}
	public List<Rewrite> Rewrites {
		get {
			return this.rewrites;
		}
	}

}

public class Logger{
	public static void logSleep(string line){
	  Console.WriteLine(line);
	  Thread.Sleep(TimeSpan.FromSeconds(0.5));
	}
}


public class SimplifyStates{
	Dictionary<String, StateHist> foundStates = new Dictionary<String, StateHist>();
	int initComplexity;
	StateHist best=null;
	Step nextStepOnTrue;
	bool solveForX=false;
	
	bool logging=false;
	public SimplifyStates (StateHist qhist)
	{
		foundStates.Add(Node.nodeString(qhist.State),qhist);
		initComplexity = complexity(qhist.State);
	}

	public int complexity(Object expr){
		if( expr is Node ){
			int subsum=0;
			foreach( Object ch in ((Node)expr).Children ){
				subsum += complexity(ch);
			}
  		    return subsum+1;
		}else{
			//if( solveForX ){
			//	return "x".Equals(expr) ? 10 : 1;
			//}
			return 1;
		}
	}

	public bool containsState(Object newExpr){
		string producedStr = Node.nodeString(newExpr);
		return foundStates.ContainsKey(producedStr);
	}

	public bool addState(StateHist newExprHist){
		if( logging ){
		  //Logger.logSleep("addState "+Node.nodeString(newExprHist.State)
		//		+" complex="+complexity(newExprHist.State));
		}

		string producedStr = Node.nodeString(newExprHist.State);
		if( ! foundStates.ContainsKey(producedStr) ){
			foundStates.Add(producedStr, newExprHist);
			if( solveForX ){
				Node state = (Node)newExprHist.State;
				if( state.Children[0].Equals("x") || state.Children[1].Equals("x") ){
					best = newExprHist;
				}
			}else{
				if( complexity(newExprHist.State)<initComplexity ){
					best = newExprHist;
					initComplexity = complexity(newExprHist.State);
				}
			}
			return true;
		}
		return false;
	}
	public int complexityDiff(){
		if( nextStepOnTrue==null ){
			return 0;
		}
		return nextStepOnTrue.complexityDiff();
	}
	public bool foundTrue(){
		return best!=null && "T".Equals(best.State);
	}
	public bool FoundResult(){
		return best!=null && ("T".Equals(best.State) || "F".Equals(best.State) || solveForX);
	}
	public StateHist Best {
		get {
			return this.best;
		}
	}
	public bool Logging {
		get {
			return this.logging;
		}
		set {
			logging = value;
		}
	}
	public bool SolveForX {
		get {
			return this.solveForX;
		}
		set {
			solveForX = value;
		}
	}
	public int InitComplexity {
		get {
			return this.initComplexity;
		}
	}
	public Step NextStepOnTrue {
		get {
			return this.nextStepOnTrue;
		}
		set {
			nextStepOnTrue = value;
		}
	}

}


public abstract class Step{
	protected SimplifyStates states;
	public Step (SimplifyStates states)
	{
		this.states = states;
	}

	public abstract void execute(Deductive deduct);
	public abstract int complexityDiff();
}
class InitStep : Step{ // entry point for expression simplification
	//Node cond;
	Object q;
	StateHist shist;
	public InitStep (SimplifyStates states, /*Node cond,*/ StateHist shist) : base(states)
	{
		//this.cond = cond;
		this.shist = shist;
		this.q = shist.State;
	}
	/*
	public Node Cond {
		get {
			return this.cond;
		}
	}
	*/
	public StateHist SHist {
		get {
			return this.shist;
		}
	}
	
	public override string ToString ()
	{
		return "InitStep "+Node.nodeString(q)+" complDiff="+complexityDiff();
	}

	override public void execute(Deductive deduct){
		foreach( Rewrite r in deduct.Rewrites ){
			//Console.WriteLine("rewrite "+Node.nodeString(r.Src)+" "+Node.nodeString(r.Target));
			List<RewriteResult> rrList = r.findReplace(q);
			foreach(RewriteResult rr in rrList){
				if( !states.containsState(rr.Res) ){
					//Console.WriteLine("calling replaceVars "+
					//	Rewrite.dictVarsToString(rr.Vars)+" "+Node.nodeString(r.Cond));
					Console.WriteLine("TODO skipped check condition using rule "+Node.nodeString(r.Src));
					//Node localCond = (Node)Rewrite.replaceVars(rr.Vars, r.Cond);
					/*
					Console.WriteLine("checking cond for "+Node.nodeString(rr.Res)
						+" cond="+Node.nodeString(localCond)+" by="+r
						+" complDiff="+(complexity(rr.Res)-states.InitComplexity));
						*/
					deduct.addStep(new CheckConditionStep(states, this, rr, /*localCond.Children*/new ArrayList()));
				}
			}
			if( states.FoundResult() ){
				return;
			}
		}
	  }
	public override int complexityDiff ()
	{
		return states.complexityDiff() +  states.complexity(q);
	}
}
class CheckConditionStep : Step{
	InitStep parent;
	RewriteResult rr;
	ArrayList condsToCheck;
	public CheckConditionStep (SimplifyStates states, InitStep parent, RewriteResult rr, ArrayList condsToCheck)
		: base(states)
	{
		this.parent = parent;
		this.rr = rr;
		this.condsToCheck = condsToCheck;
	}
	
	public override int complexityDiff (){
		return states.complexityDiff() + states.complexity(rr.Res);
	}
	
	public override string ToString ()
	{
		return "CheckConditionStep for ["+parent+"] complDiff="+complexityDiff();
	}

	override public void execute(Deductive deduct){
		if( !states.containsState(rr.Res) ){
			if( condsToCheck.Count==0 ){
				// now all conditions satisfied, we can use the resulting rewritten expression
				Logger.logSleep("adding state "+Node.nodeString(rr.Res));
				states.addState(parent.SHist.chain(rr.Res));
				if( states.foundTrue() ){
					if( states.NextStepOnTrue!=null ){
						//if( "T".Equals(states.Best.State) ){
							deduct.addStep(states.NextStepOnTrue);
						//}else{
							//Console.WriteLine("finished with non-T result "+Node.nodeString(states.Best));
						//}
					}
					// we found smth simpler, so we finished
				}else if( states.FoundResult() ){
					// stop rewriting - simplest possible form found
				}else{
					// continue rewriting
					deduct.addStep(new InitStep(states, /*parent.Cond,*/ new StateHist(rr.Res, parent.SHist)));
				}
			}else{
				Step nextStep = new CheckConditionStep(states, parent, rr, 
						condsToCheck.GetRange(1, condsToCheck.Count-1));
				
				Object cneed = condsToCheck[0];
				//Node withConditions = parent.Cond;
				//Console.WriteLine("need satisfy cond "+Node.nodeString(cneed)+ " for "+parent.SHist.fullHistory());
				bool found=false;
				/*
				foreach( Object cknown in withConditions.Children ){
				   if( Node.eq(cknown, cneed) ){
					  found=true;
					  break;
					}
				}*/
				
				if( found ){
					deduct.addStep(nextStep);
				}
				/*
				if( !found ){
					Node condSubQuest = new Node("?");
					condSubQuest.add(withConditions);
					condSubQuest.add(cneed);
					//Console.WriteLine("need simplify "+Node.nodeString(condSubQuest)+" for "+parent.SHist.fullHistory());
					
					StateHist shist = new StateHist(cneed,null);
					SimplifyStates subStates = new SimplifyStates(shist);
					subStates.NextStepOnTrue = nextStep;
					InitStep subStep = new InitStep(subStates, withConditions, shist);
					deduct.addStep(subStep);

				}
				*/
			}
		}
	}		
}



public class Deductive
{
	RewritesBase rewritesBase;
	List<Rewrite> rewrites;
	List<Step> steps = new List<Step>();
	int totalStepsExec=0;
	
	public Deductive (RewritesBase rewrBase)
	{
		this.rewrites = rewrBase.Rewrites;
		this.rewritesBase = rewrBase;
	}
	
	public void addStep(Step step){
		steps.Add(step);
	}
	
	public List<Rewrite> Rewrites {
		get {
			return this.rewrites;
		}
	}

    int minComplexityDiff(List<Step> stepsList){
	  bool first=true;
	  int min=0;
	  foreach(Step s in stepsList){
		int diff = s.complexityDiff();
		if( first || diff<min ){
			min=diff;
		}
		first=false;
	  }
	  return min;
    }
    
	void execSteps(SimplifyStates states){
		List<Step> stepsNew = new List<Step>(steps);
		steps.Clear();
	    int minDiff = minComplexityDiff(stepsNew);
	    int done=0;
	    int skipped=0;
		foreach( Step step in stepsNew ){
		    if( step.complexityDiff()==minDiff ){
			  //Logger.logSleep("executing "+step);
			  totalStepsExec++;
			  step.execute(this);
			  done++;
		    }else{
			  skipped ++;
			  steps.Add(step); // postpone
		    }
			if( states.FoundResult() ){
				return;
			}
		}
	    //Console.WriteLine("minDiff was "+minDiff+" done="+done+" postponed="+skipped);
	}
	
	
	

	public StateHist simplify(bool solveForX, /*Node cond,*/ Node q){
		Console.WriteLine("starting simplify rewrites="+rewrites.Count);
		StateHist shist = new StateHist(q,null);
		SimplifyStates states = new SimplifyStates(shist);
		states.SolveForX=solveForX;
		states.Logging=true;
		steps.Add(new InitStep(states, /*cond,*/ shist));
		
		var bestStr = "";
		for( int i=0; i<5; i++ ){
		//for( int i=0; i<60; i++ ){
			execSteps( states );
			if( states.Best!=null ){
		      var bestStrNow = Node.nodeString(states.Best.State);
		      if( !bestStrNow.Equals(bestStr) ){
				bestStr = bestStrNow;
	  			Console.WriteLine("  search depth "+i+" stepsQ="+steps.Count+" best="+bestStr);
  			  }
			}
			if( states.FoundResult() ){
				break;
			}
		}
		if( states.FoundResult() ){
			rewritesBase.add(/*cond,*/ q, states.Best.State);
		}
		if( states.Best!=null ){
			Console.WriteLine("totalStepsExec=" + totalStepsExec);
			Console.WriteLine("  newCompl="+states.complexity(states.Best.State)+"  res="+Node.nodeString(states.Best.State));
			return states.Best;
		}
		return null;
	}



}



